COMMENT ⊗   VALID 00002 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	% Handles non-situation-dependent at more better than previous versions.
C00006 ENDMK
C⊗;
% Handles non-situation-dependent at more better than previous versions.

% Contains additional declarations and axioms for reifying actions.

declare INDVAR x y z s p a1 a2;

declare INDCONST I, S0, desk, home,car,airport,county;

declare PREDCONST at 3, att 2, walkable 1, drivable 1;

declare OPCONST walk 2, drive 2, result 3, prog 2, walka 1, drivea 1;

axiom walkable:	walkable(home);;

axiom drivable:	drivable(county);;

axiom at:
	at(I,desk,S0)
	att(desk,home)
	at(car,home,S0)
	att(home,county)
	att(airport,county)
;;

axiom ats:	∀x y.(att(x,y) ⊃ ∀s.at(x,y,s));;

axiom attrans:
	∀x y z s.(at(x,y,s) ∧ at(y,z,s) ⊃ at(x,z,s))
	∀x y z.(att(x,y) ∧ att(y,z) ⊃ att(x,z))
;;

axiom walk:
	∀x y z s.((walkable(x) ∧ (att(y,x)∨at(y,x,s)) ∧ (att(z,x)∨at(z,x,s))
			 ∧ at(I,y,s))
		⊃ (at(I,z,walk(z,s))
		   ∧ ∀x y.(¬(x = I) ⊃ (at(x,y,walk(z,s)) ≡ at(x,y,s)))))
;;

axiom drive:
	∀x y z s.((drivable(x) ∧ att(y,x) 
				∧ att(z,x) ∧ at(car,y,s) ∧ at(I,car,s))
		⊃ (at(car,z,drive(z,s))
			∧ ∀x y.(¬(x = car ∨ at(x,car,s)) ∨ y=car
					 ⊃ (at(x,y,drive(z,s)) ≡ at(x,y,s)))))
;;

axiom notI:	¬(I=desk) ∧ ¬(I=car) ∧ ¬(I=home) ∧ ¬(I=airport);;

axiom walka:
	∀x y z p s.((walkable(x) ∧ (att(y,x)∨at(y,x,s)) ∧ (att(z,x)∨at(z,x,s))
			 ∧ at(p,y,s))
		⊃ (at(p,z,result(p,walka(z),s))
		   ∧ ∀x y.(¬(x = I) ⊃ (at(x,y,result(p,walka(z),s)) ≡ at(x,y,s)))))
;;

axiom drivea:
	∀x y z p s.((drivable(x) ∧ att(y,x) 
				∧ att(z,x) ∧ at(car,y,s) ∧ at(p,car,s))
		⊃ (at(car,z,result(p,drivea(z),s))
		∧ ∀x y.(¬(x = car ∨ at(x,car,s)) ∨ y=car
			 ⊃ (at(x,y,result(p,drivea(z),s)) ≡ at(x,y,s)))))
;;

axiom prog:
	∀a1 a2 p s.(result(p,prog(a1,a2),s) = result(p,a2,result(p,a1,s)))
;;

% The next two axioms make axioms  walk  and  drive  redundant.

axiom walkb:
	∀x s.(walk(x,s) = result(I,walka(x),s))
;;

axiom driveb:
	∀x s.(drive(x,s) = result(I,drivea(x),s))
;;